the_w:World, l:IdLnk, t:. rcvs(l;t)  Action(destination(l)) List 

latex

Definitions	rcvs(l;t), filter(P;l), destination(l), isrcv(l;a), map(f;as), Action(i), a(i;t), i  j < k, P & Q, AB, {i..j}, upto(n), x:A. B(x), , IdLnk, t  T, World
Lemmas	world wf, IdLnk wf, nat wf, upto wf, int seg wf, le wf, w-a wf, map wf, w-isrcvl wf, ldst wf, w-action wf, filter wf